deferred predicate # : (int * int) ~> prop
where forall x. x # (x + 1)
lemma : 1 # (1 + 1)
